iv class="head">
Theory Prelim
section â¹Preliminaries⺠theory Prelim imports "Bounded_Deducibility_Security.Compositional_Reasoning" "Fresh_Identifiers.Fresh_String" begin subsectionâ¹The basic types⺠definition "emptyStr = STR ''''" (* The users of the system: *) datatype name = Nam String.literal definition "emptyName â¡ Nam emptyStr" datatype inform = Info String.literal definition "emptyInfo â¡ Info emptyStr" datatype user = Usr (nameUser : name) (infoUser : inform) definition "emptyUser â¡ Usr emptyName emptyInfo" fun niUser where "niUser (Usr name info) = (name,info)" typedecl raw_data code_printing type_constructor raw_data â (Scala) "java.io.File" (* Images (currently, pdf, to be changed): *) datatype img = emptyImg | Imag raw_data (* Visibility outside the current api: either friends-only or public *) datatype vis = Vsb String.literal (* Accepted values: friend and public *) abbreviation "FriendV â¡ Vsb (STR ''friend'')" abbreviation "PublicV â¡ Vsb (STR ''public'')" fun stringOfVis where "stringOfVis (Vsb str) = str" (* A post consists of a string for title, a string for its text, a (possibly empty) image and a visibility specification: *) datatype title = Tit String.literal definition "emptyTitle â¡ Tit emptyStr" datatype "text" = Txt String.literal definition "emptyText â¡ Txt emptyStr" datatype post = Ntc (titlePost : title) (textPost : "text") (imgPost : img) (* Setters: *) fun setTitlePost where "setTitlePost (Ntc title text img) title' = Ntc title' text img" fun setTextPost where "setTextPost(Ntc title text img) text' = Ntc title text' img" fun setImgPost where "setImgPost (Ntc title text img) img' = Ntc title text img'" (* *) definition emptyPost :: post where "emptyPost â¡ Ntc emptyTitle emptyText emptyImg" (* initially set to the lowest visibility: friend *) lemma set_get_post[simp]: "titlePost (setTitlePost ntc title) = title" "titlePost (setTextPost ntc text) = titlePost ntc" "titlePost (setImgPost ntc img) = titlePost ntc" (* *) "textPost (setTitlePost ntc title) = textPost ntc" "textPost (setTextPost ntc text) = text" "textPost (setImgPost ntc img) = textPost ntc" (* *) "imgPost (setTitlePost ntc title) = imgPost ntc" "imgPost (setTextPost ntc text) = imgPost ntc" "imgPost (setImgPost ntc img) = img" by(cases ntc, auto)+ datatype password = Psw String.literal definition "emptyPass â¡ Psw emptyStr" (* Information associated to requests for registration: both for users and apps *) datatype req = ReqInfo String.literal definition "emptyReq â¡ ReqInfo emptyStr" subsection â¹Identifiers⺠datatype userID = Uid String.literal datatype postID = Nid String.literal definition "emptyUserID â¡ Uid emptyStr" definition "emptyPostID â¡ Nid emptyStr" (* *) fun userIDAsStr where "userIDAsStr (Uid str) = str" definition "getFreshUserID userIDs â¡ Uid (fresh (set (map userIDAsStr userIDs)) (STR ''2''))" lemma UserID_userIDAsStr[simp]: "Uid (userIDAsStr userID) = userID" by (cases userID) auto lemma member_userIDAsStr_iff[simp]: "str â userIDAsStr ` (set userIDs) â· Uid str ââ userIDs" by (metis UserID_userIDAsStr image_iff userIDAsStr.simps) lemma getFreshUserID: "¬ getFreshUserID userIDs ââ userIDs" using fresh_notIn[of "set (map userIDAsStr userIDs)"] unfolding getFreshUserID_def by auto (* *) fun postIDAsStr where "postIDAsStr (Nid str) = str" definition "getFreshPostID postIDs â¡ Nid (fresh (set (map postIDAsStr postIDs)) (STR ''3''))" lemma PostID_postIDAsStr[simp]: "Nid (postIDAsStr postID) = postID" by (cases postID) auto lemma member_postIDAsStr_iff[simp]: "str â postIDAsStr ` (set postIDs) â· Nid str ââ postIDs" by (metis PostID_postIDAsStr image_iff postIDAsStr.simps) lemma getFreshPostID: "¬ getFreshPostID postIDs ââ postIDs" using fresh_notIn[of "set (map postIDAsStr postIDs)"] unfolding getFreshPostID_def by auto end